package srt.tool;

import java.io.IOException;
import java.util.ArrayList;
import java.util.List;

import srt.ast.AssertStmt;
import srt.ast.Invariant;
import srt.ast.InvariantList;
import srt.ast.Program;
import srt.ast.WhileStmt;
import srt.ast.visitor.impl.DefaultVisitor;
import srt.exec.ProcessExec;
import srt.tool.SRTool.SRToolResult;
import srt.tool.exception.ProcessTimeoutException;

//Visitor implementation for Houdini algorithm of 
//selection appropriate candidate invariants
public class HoudiniVisitor extends DefaultVisitor {

	CLArgs clArgs = new CLArgs();
	private List<WhileStmt> whileNodes = new ArrayList<WhileStmt>();
	private List<AssertStmt> allAssertionNodes = new ArrayList<AssertStmt>();

	private Program programCopy;

	public HoudiniVisitor() {
		super(true);
	}

	@Override
	public Object visit(Program program) {
		//evaluation of the initial programm
		programCopy = program;

		CollectConstraintsVisitor ccv = new CollectConstraintsVisitor();
		ccv.visit(program);

		whileNodes = ccv.whileNodes;

		program = (Program) new LoopAbstractionVisitor().visit(program);

		ccv = new CollectConstraintsVisitor();
		ccv.visit(program);

		allAssertionNodes = ccv.propertyNodes;

		program = (Program) new PredicationVisitor().visit(program);

		program = (Program) new SSAVisitor().visit(program);

		ccv = new CollectConstraintsVisitor();
		ccv.visit(program);

		SMTLIBQueryBuilder builder = new SMTLIBQueryBuilder(ccv);
		builder.buildQuery();

		String smtQuery = builder.getQuery();

		ProcessExec process = new ProcessExec("z3", "-smt2", "-in");
		String queryResult = "";
		try {
			queryResult = process.execute(smtQuery, clArgs.timeout);
		} catch (ProcessTimeoutException e) {
			if (clArgs.verbose) {
				System.out.println("Timeout!");
			}
			return SRToolResult.UNKNOWN;
		} catch (InterruptedException e1) {
			e1.printStackTrace();
		} catch (IOException e2){
			e2.printStackTrace();
		}
		
		//Houdini algorithm check if program is correct return
		//else if program is incorrect and all candidate invariants holds return
		//else disable failing candidates and run houdini again
		if (queryResult.startsWith("sat")) {

			queryResult = queryResult.substring(queryResult.indexOf('\n') + 1);

			queryResult = queryResult.replaceAll("\\(", "").replaceAll("\\)",
					"");
			
			String[] lines = queryResult.split("\\r?\\n");

			boolean tmp = true;

			List<Invariant> tmpInvariantList = new ArrayList<Invariant>();
			List<Invariant> invariantsToDelete = new ArrayList<Invariant>();
			List<WhileStmt> newWhileNodes = new ArrayList<WhileStmt>();

			for (WhileStmt whileStmt : whileNodes) {
				tmpInvariantList = whileStmt.getInvariantList().getInvariants();
				invariantsToDelete = new ArrayList<Invariant>();
				for (Invariant inv : tmpInvariantList) {
					for (AssertStmt assertion : allAssertionNodes) {
						if (inv.getExpr() == assertion.getCondition()
								&& lines[allAssertionNodes.indexOf(assertion)]
										.contains("true") && inv.isCandidate()) {
							invariantsToDelete.add(inv);
							tmp = false;
						} 
					}
				}
				tmpInvariantList.removeAll(invariantsToDelete);
				
				newWhileNodes.add(new WhileStmt(whileStmt.getCondition(),
						whileStmt.getBound(), new InvariantList(
								new ArrayList<Invariant>(tmpInvariantList)),
						whileStmt.getBody()));

			}
			

			if (!tmp) {
				programCopy = (Program) new ReplacementVisitor(newWhileNodes)
						.visit(programCopy);
				
				
				visit(programCopy);
			} else {
				programCopy = (Program) new ReplacementVisitor(whileNodes)
						.visit(programCopy);
				return programCopy;
			}
		}

		return programCopy;

	}

}
